%%% SetCons.oz
%
% This module uses the "set" model of the field to propagate and
% search for solutions.  This models refines the binary model.  It
% considers subsets of binary variables, and reformulates the binary
% constraints in terms of these sets.  This allows for infering
% information about groups of squares, without knowing anything about
% the individual squares.
%
% SetCons.propagator
%    creates a propagator for the field F.  This propagator posts a
%    given constraint C as several propagators on subsets of binary
%    variables.  If C is
%
%         B1+...+Bn=K,
%
%    and all Bi are nondetermined, it will use one FD variable for
%    each subset of {B1,...,Bn}, representing the sum of the subset.
%    It will then post one propagator for each partition of
%    {B1,...,Bn}.  If n=4, this gives (all terms in parentheses stand
%    for their FD variable)
%
%         (B1)+(B2)+(B3)+(B4)=K, (B1+B2)+(B3)+(B4)=K,
%         (B2)+(B1+B3)+(B4)=K, (B2)+(B3)+(B1+B4)=K,
%         (B1)+(B2+B3)+(B4)=K, (B1)+(B3)+(B2+B4)=K,
%         (B1)+(B2)+(B3+B4)=K, (B1+B2)+(B3+B4)=K, (B1+B3)+(B2+B4)=K,
%         (B2+B3)+(B1+B4)=K, (B1)+(B2+B3+B4)=K, (B2)+(B1+B3+B4)=K,
%         (B3)+(B1+B2+B4)=K, (B1+B2+B3)+(B4)=K, (B1+B2+B3+B4)=K
%
% SetCons.solver
%    implements a search engine similar to BinCons.solver.  It
%    partitions the set of binary variables in order to eliminate
%    symmetries in the problem.  Given constraints Cs, the set
%    {B1,...,Bn} is symmetric if the variables Bi are always summed
%    together in Cs.  In other words, every constraint C either
%    involves B1+...+Bn, or does not mention any of the Bi.  The
%    partition contains all the maximal symmetric subsets.
%
functor
import
   FD
   Field      at 'Field.ozf'
   Game       at 'Game.ozf'
   LazySearch at 'LazySearch.ozf'

export
   Propagator
   Solver

define
   % The "set" propagator
   class Propagator from Game.switchable
      meth init(F Cs)
	 N = {Width F}
	 B = {FD.tuple {Label F} N 0#1}
	 fun {BF I} B.I end

	 % FD var corresponding to subset of indexes
	 Set = {NewDictionary}
	 Deprecated = local Str in
			 thread   % removes the deprecated sets from Set
			    for K#_ in Str do {Dictionary.remove Set K} end
			 end
			 {NewWeakDictionary Str}
		      end

	 proc {SetF Is ?S}
	    % Assumption: Is is sorted
	    Key = {FoldL Is fun {$ K I} K*N+I end 0}
	 in
	    try
	       S = Set.Key
	    catch _ then
	       BinVars = {Map Is BF}
	    in
	       S = {FD.decl}   {FD.sum BinVars '=:' S}   Set.Key := S
	       % deprecate a set as soon as one of BinVars is known
	       {WeakDictionary.put Deprecated Key
		thread {Record.waitOr {List.toTuple bin BinVars}} end}
	    end
	 end
      in
	 % create propagators from Cs
	 thread
	    case Cs of sum(Is K)|Cr then
	       {FD.sum {Map Is BF} '=:' K}   % special case

	       for sum(Is K) in Cr do Known Unknown in
		  {Wait @enabled}
		  {List.partition Is fun {$ I} {IsDet B.I} end Known Unknown}
		  case {Sort Unknown Value.'<'} of (Js = _|_) then
		     % post a propagator for each partition of the unknowns
		     for P in {Partitions Js} do
			{FD.sum {Append {Map P SetF} {Map Known BF}} '=:' K}
		     end
		  else skip end
	       end
	    end
	 end

	 % put results back in F
	 F = {Record.map B fun {$ X} thread {Field.symbolic X} end end}
      end
   end

   % returns all the partitions of the non-empty set Xs.  Each
   % partition is a list of subsets of Xs, and each subset is a
   % subsequence of Xs (subsets are ordered as in Xs).
   fun lazy {Partitions Xs}
      case Xs of [X] then
	 [[X]]|nil
      [] X|Xr then Ps = {Partitions Xr} in
	 {LConcat
	  {LMap Ps
	   fun {$ P}
	      % returns P where X has been inserted in P's N-th subset
	      fun {InsertAt N _} {MapNth P N fun {$ S} X|S end} end
	   in
	      ([X]|P) | {LMapInd P InsertAt}
	   end}}
      end
   end

   % useful functions (mostly lazy)
   fun lazy {LMap Xs F}
      case Xs of X|Xr then {F X}|{LMap Xr F} else nil end
   end
   fun lazy {LAppend Xs Ys}
      case Xs of X|Xr then X|{LAppend Xr Ys} else Ys end
   end
   fun lazy {LConcat Xss}
      case Xss of Xs|Xsr then {LAppend Xs {LConcat Xsr}} else nil end
   end
   fun {LMapInd Xs F} {LazyMapInd Xs 1 F} end
   fun lazy {LazyMapInd Xs I F}
      case Xs of X|Xr then {F I X}|{LazyMapInd Xr I+1 F} else nil end
   end
   fun {MapNth Xs N F} % maps F only on the N-th element of Xs
      case Xs of X|Xr then
	 if N =< 1 then {F X}|Xr else X|{MapNth Xr N-1 F} end
      else nil end
   end

   % solves the binary problem
   class Solver
      attr
	 constraints: nil   % stack with all the constraints

      meth init(Cs)
	 thread
	    for C in Cs do Cr in Cr = constraints := C|Cr end
	 end
      end

      meth search(common: Common <= _
		  mean:   Mean   <= _
		  found:  Found  <= _
		  total:  Total  <= _)
	 Cs = {Reverse @constraints}
	 Indexes = Cs.1.1

	 local
	    % maps each index to a name
	    NameOf = {NewDictionary}
	    for I in Indexes do NameOf.I := unit end

	    % computes the optimal partition
	    Moved = {NewDictionary}
	    for sum(Is _) in Cs do
	       {Dictionary.removeAll Moved}
	       for I in Is do
		  N = NameOf.I
	       in
		  if {Not {Dictionary.member Moved N}} then
		     Moved.N := {NewName} end
		  NameOf.I := Moved.N
	       end
	    end

	    % maps each name to its index list (inverse of NameOf)
	    VarsOf = {NewDictionary}
	    for I#N in {Dictionary.entries NameOf} do
	       VarsOf.N := I | {CondSelect VarsOf N nil}
	    end
	 in
	    % makes a tuple of NameTo (subset are numbered)
	    Elements = {List.toTuple vars {Dictionary.items VarsOf}}

	    % size of each set in the partition
	    Size = {Record.map Elements Length}

	    % maps each index to its corresponding set index
	    Set = {Tuple.make partition {Length Indexes}}
	    {Record.forAllInd Elements
	     proc {$ S Is} for I in Is do Set.I = S end end}
	 end

	 % reformulates the constraints in the partition model
	 Ps = {Map Cs fun {$ sum(Is K)}
			 Used = {NewDictionary}
		      in % put all set numbers used in Used
			 for I in Is do Used.(Set.I) := unit end
			 sum({Dictionary.keys Used} K)
		      end}

	 % script of the reformulated problem
	 proc {Script Sol}
	    Sol = {Record.map Size fun {$ K} {FD.int 0#K} end}
	    for sum(Ss K) in Ps do
	       {FD.sum {Map Ss fun {$ S} Sol.S end} '=:' K}
	    end
	    {FD.distribute ff Sol}
	 end

	 % sum of all solutions in the initial problem
	 Sum    = {Array.new 1 {Length Indexes} 0}
	 TotalC = {NewCell 0}
	 FoundC = {NewCell 0}
	 for Sol in {LazySearch.all Script} do
	    % number of solutions for each partition
	    Symmetric = {Record.zip Size Sol Binomial}
	    % number of solutions for all partitions
	    NumSym = {Record.foldL Symmetric Number.'*' 1}
	 in
	    % for each set in the partition, add the solutions
	    for S in 1..{Width Elements} do
	       W = NumSym * Sol.S div Size.S   % weight of each element
	    in
	       for I in Elements.S do Sum.I := Sum.I + W end
	    end
	    % add to the counters
	    TotalC := @TotalC + NumSym
	    FoundC := @FoundC + 1
	 end

	 SumField = {Array.toRecord field Sum}
      in
	 Total = @TotalC
	 Found = @FoundC

	 Common = {Record.map SumField
		   fun {$ X}
		      case X of 0 then 0 [] !Total then 1 else _ end
		   end}
	 Mean   = {Record.map SumField
		   fun {$ X} {IntToFloat X} / {IntToFloat Total} end}
      end
   end

   % computes the binomial number C(N,K)
   fun {Binomial N K}
      if K<0 then 0
      elseif K==0 orelse K==N then 1
      else {Binomial N-1 K-1} * N div K
      end
   end
end
